DROPS

Document

DOI: 10.4230/OASIcs.FMBC.2020.4

Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts

Authors: João Santos Reis, Paul Crocker, and Simão Melo de Sousa

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)

Abstract

This paper introduces Tezla, an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and aims to preserve the semantics, flow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified. We provide an automated decompiler of Michelson smart contracts to Tezla. In order to support our claim about the adequacy of Tezla, we develop a static analyser that takes advantage of the Tezla representation of Michelson smart contracts to prove simple but non-trivial properties.

Cite as

João Santos Reis, Paul Crocker, and Simão Melo de Sousa. Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 4:1-4:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{santosreis_et_al:OASIcs.FMBC.2020.4,
  author =	{Santos Reis, Jo\~{a}o and Crocker, Paul and Melo de Sousa, Sim\~{a}o},
  title =	{{Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{4:1--4:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.4},
  URN =		{urn:nbn:de:0030-drops-134176},
  doi =		{10.4230/OASIcs.FMBC.2020.4},
  annote =	{Keywords: Intermediate representation, Static analysis, Tezos blockchain, Michelson}
}

Search Results

Documents authored by Crocker, Paul

Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts

Abstract

Cite as

Thanks for your feedback!

Could not send message